A simple sequent calculus for nominal logic

摘要

Nominal logic is a variant of first-order logic that provides support forreasoning about bound names in abstract syntax. A key feature of nominal logicis the new-quantifier, which quantifies over fresh names (names not appearingin any values considered so far). Previous attempts have been made to developconvenient rules for reasoning with the new-quantifier, but we argue that noneof these attempts is completely satisfactory. In this article we develop a new sequent calculus for nominal logic in whichthe rules for the new- quantifier are much simpler than in previous attempts.We also prove several structural and metatheoretic properties, includingcut-elimination, consistency, and equivalence to Pitts' axiomatization ofnominal logic.